the_es:ES, e:E, l:IdLnk. haslnk(l;e)  isrcv(e) & lnk(e) = l 

latex

Definitions	ES, E, haslnk(l;e), p  q, Unit, isrcv(e), , b, A, b, a = b, True, P  Q, P & Q, P  Q, Prop, IdLnk, lnk(e), x:A. B(x), P  Q, t  T, False, A & B
Lemmas	es-lnk wf, false wf, true wf, eq lnk wf, assert wf, assert-eq-lnk, iff functionality wrt iff, not wf, bnot wf, bool wf, es-isrcv wf, assert of bnot, eqff to assert, iff transitivity, eqtt to assert, IdLnk wf, es-E wf, event system wf